\begin{tabbing}
cr{-}antecedent\{i:l\}(${\it es}$; ${\it Config}$; ${\it Cmd}$; ${\it Sys}$; $u$)($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if\= csinput?(${\it Sys}$($e$))\+\+
\\[0ex]then $e$
\-\\[0ex]if\= ($u$($e$)) $\in_{b}$ ${\it Config}$\+
\\[0ex]then es{-}prior{-}interface\=\{i:l\}\+
\\[0ex](${\it es}$; sys{-}valid\{i:l\}(${\it es}$; ${\it Config}$; ${\it Cmd}$; ${\it Sys}$))($u$($e$))
\-\-\\[0ex]else $u$($e$)
\\[0ex]fi 
\-
\end{tabbing}